FDL - Nuprl Lemma : causal-bijection-interleaving

Nuprl Lemma : causal-bijection-interleaving

es:ES, P, Q:(E

), f:({e:E| P(e)}

{e:E| Q(e)} ).
Bij({e:E| P(e)} ;{e:E| Q(e)} ;f)

(

e:{e:E| P(e)} . e c

f(e))

e.f(e) is c< preserving on e.P(e)

(

e, e':{e:E| P(e)} . (

(e' < e))

e c

e')

(

e, e':{e:E| P(e)} . (e < e')

(

a:{e:E| Q(e)} . ((e < a) & (a < e'))))

(

e:E. P(e)

(

a:E. Q(a)

e c

a

(a < f(e))

False))

Definitions P Q, e c e', t ...$L, False, x. t(x), t T, P & Q, x:A. B(x), P Q, x(s), , x:A. B(x), A, a.f(a) is c< preserving on e.P(e), Dec(P), Surj(A;B;f), Inj(A;B;f), Bij(A;B;f), {T}, WellFnd{i}(A;x,y.R(x;y))

Lemmas es-causl irreflexivity, decidable es-E-equal, es-le weakening eq, es-causle weakening locl, es-causl transitivity2, es-causle weakening, decidable es-causl, es-causl-wellfnd, false wf, event system wf, es-E wf, biject wf, causal-order-preserving wf, es-causle wf, not wf, es-causl wf